Nuprl Definition : es-ble
11,40
postcript
pdf
es-ble{i:l}(
es
;
e
;
e'
)
== case TERMOF{
decidable
es-le
:ObjectId, 1:l, i:l}(
es
,
e'
,
e
) of inl(
x
) => tt | inr(
x
) => ff
latex
clarification:
es-ble{i:l}
es-ble
(
es
;
e
;
e'
)
== case TERMOF{
decidable
es-le
:ObjectId, 1:l, i:l}(
es
,
e'
,
e
) of inl(
x
) => tt | inr(
x
) => ff
latex
Definitions
ff
,
tt
,
decidable
es-le
FDL editor aliases
es-ble
origin